/**
 * Copyright (c) 2010 by Kevin Bierhoff.
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *    1. Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *    2. Redistributions in binary form must reproduce the above copyright
 *       notice, this list of conditions and the following disclaimer in the
 *       documentation and/or other materials provided with the distribution.
 *    3. Neither the names of the authors nor the
 *       names of its contributors may be used to endorse or promote products
 *       derived from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE AUTHORS ''AS IS'' AND ANY
 * EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 * WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY
 * DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 * INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
 * LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
 * ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
package com.googlecode.syper.javasyp.checker;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collection;
import java.util.Collections;
import java.util.HashMap;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.Map.Entry;

import org.eclipse.jdt.core.dom.AST;
import org.eclipse.jdt.core.dom.ArrayAccess;
import org.eclipse.jdt.core.dom.Assignment;
import org.eclipse.jdt.core.dom.CastExpression;
import org.eclipse.jdt.core.dom.Expression;
import org.eclipse.jdt.core.dom.FieldAccess;
import org.eclipse.jdt.core.dom.ITypeBinding;
import org.eclipse.jdt.core.dom.IVariableBinding;
import org.eclipse.jdt.core.dom.Modifier;
import org.eclipse.jdt.core.dom.ParenthesizedExpression;
import org.eclipse.jdt.core.dom.QualifiedName;
import org.eclipse.jdt.core.dom.SimpleName;
import org.eclipse.jdt.core.dom.ThisExpression;
import org.eclipse.jdt.core.dom.InfixExpression.Operator;

import com.googlecode.syper.javasyp.formulae.Field;
import com.googlecode.syper.javasyp.formulae.Formula;
import com.googlecode.syper.javasyp.formulae.Fun;
import com.googlecode.syper.javasyp.formulae.Infix;
import com.googlecode.syper.javasyp.formulae.Literal;
import com.googlecode.syper.javasyp.formulae.Local;
import com.googlecode.syper.javasyp.formulae.Name;
import com.googlecode.syper.javasyp.formulae.Prefix;
import com.googlecode.syper.javasyp.formulae.Quantifier;
import com.googlecode.syper.javasyp.formulae.Select;

/**
 * @author kevin
 * @since May 30, 2010
 * @param T the concrete subclass type, for, e.g., {@link #createClone()}
 */
abstract class AbstractHavocLookup<T extends AbstractHavocLookup<T>>
implements ExpressionEncoder.Lookup {

	/** Internal counter to produce unique temp variable names */
	private static int nextTemp = 0;

	/** {@link Object}'s type binding in the current AST */
	protected final ITypeBinding objType;
	/** {@code int}'s type binding in the current AST */
	protected final ITypeBinding intType;
	/** type normalization in {@link #getHeapType(ITypeBinding)} */
	private final TypeNormalizer types;

	/** Keeps track of temps for intermediary expressions */
	private final Map<Expression, Local> temps;

	/** Maps local variables to their incarnations (bumped when havoc'ed) */
	private final Map<IVariableBinding, Integer> locals;

	/** Maps array heaps to their incarnations */
	private final Map<ITypeBinding, Integer> arrays;

	/**
	 * Use this constructor to create a fresh lookup.
	 */
	public AbstractHavocLookup(AST ast) {
		types = new TypeNormalizer(ast);
		objType = types.getObjectType();
		intType = ast.resolveWellKnownType("int");
		temps = new HashMap<Expression, Local>();
		locals = new HashMap<IVariableBinding, Integer>();
		arrays = new HashMap<ITypeBinding, Integer>();
	}

	/** Copy-constructor (from any {@link AbstractHavocLookup}) */
	protected AbstractHavocLookup(AbstractHavocLookup<?> original) {
		// shared type lookup since clones should be over a single AST instance
		types = original.types;
		objType = original.objType;
		intType = original.intType;
		// temps must be shared to ensure unique mapping from expressions to temps
		temps = original.temps;
		// locals and arrays can be on different heap incarnations
		locals = new HashMap<IVariableBinding, Integer>(original.locals);
		arrays = new HashMap<ITypeBinding, Integer>(original.arrays);
	}

	/**
	 * TODO obsolete??
	 * @param n
	 * @return
	 */
	public abstract Collection<Field> getKnownFields(Name n);

	/**
	 * for re-assigning variables or fields locally
	 * @param es expressions to havoc
	 * @param aroundLoop TODO
	 * @return information that shouldn't be lost, never {@code null}
	 */
	public abstract Collection<Formula> havoc(Collection<Expression> es, boolean aroundLoop);

	/**
	 * for havoc-ing fields of method parameters
	 * @param modified map from parameters to fields to havoc; a {@code null}
	 * value in the field set denotes the contents of an array parameter
	 * @return information that shouldn't be lost, never {@code null}
	 */
	public abstract Collection<Formula> havoc(Map<Name, ? extends Collection<IVariableBinding>> modified);

	/**
	 * Creates a clone with independent havoc'ing information.
	 * @return a clone with independent havoc'ing information.
	 */
	public abstract T createClone();

	public Local getLocal(Expression e) {
		if (e instanceof ThisExpression)
			return new Local(e.toString(), e.resolveTypeBinding());
		if (e instanceof SimpleName)
			return getLocal((SimpleName) e);
		if (e instanceof ParenthesizedExpression)
			return getLocal(((ParenthesizedExpression) e).getExpression());
		if (e instanceof CastExpression)
			return getLocal(((CastExpression) e).getExpression());
		if (e instanceof Assignment)
			return getLocal(((Assignment) e).getLeftHandSide());
		Local temp = temps.get(e);
		if (temp == null) {
			temp = new Local("temp" + (nextTemp++), e.resolveTypeBinding());
			temps.put(e, temp);
		}
		return temp;
	}

	/**
	 * Helper method for havoc'ing a local variable in
	 * {@link #havoc(Collection, boolean)}
	 * @param binding must be a local variable (including parameters)
	 */
	protected final void havocLocal(IVariableBinding binding) {
		if (binding.isField() || binding.isEnumConstant())
			throw new IllegalArgumentException("Not a local: " + binding);
		Integer incarnation = locals.get(binding);
		if (incarnation != null)
			locals.put(binding, incarnation + 1);
	}

	/**
	 * Havocs all heap cells except contents of the given references
	 * and final fields.
	 * This implementation havocs array contents.
	 * Override this method to havoc additional parts of the heap.
	 * @param keep objects to keep with their array permissions, if applicable
	 * @param modifiable Set from modifiable objects to the fields of
	 * these objects that may be modified; in addition, objects reachable
	 * from the given objects may be modifiable.
	 * @return Formulae preserving information about {@code keepers}
	 */
	protected final Collection<Formula> havocArrays(Map<Name, PermKind[]> keep,
			Map<Name, ? extends Collection<IVariableBinding>> modifiable) {
		List<Formula> result = new ArrayList<Formula>(arrays.size());
		String protectPred = getProtectionPredicate(objType);
		// havoc known array heaps except keepers but including modifiable array parameters
		// TODO only exclude keepers that are really arrays (shorter assertion) but make sure arrays protected by keepers are not forgotten
		for (Map.Entry<ITypeBinding, Integer> h : arrays.entrySet()) {
			int oldIncarnation = h.getValue();
			int newIncarnation = oldIncarnation + 1;
			h.setValue(newIncarnation);

			if (keep.isEmpty())
				// havoc all arrays
				continue;

			Local objVar = new Local("o'", objType);
			Local indexVar = new Local("i'", intType);

			Set<Formula> toKeep = new LinkedHashSet<Formula>();
			for (final Map.Entry<Name, PermKind[]> k : keep.entrySet()) {
				final Name n = k.getKey();
				Collection<IVariableBinding> mod = modifiable.get(n);
				if (mod != null && mod.contains(null))
					// array cells are modifiable, so don't keep this one
					continue;
				toKeep.add(Infix.equals(n, objVar));
				if (protectPred != null && mod == null)
					// protect arrays reachable from keepers through fields with permissions
					// 1. protection predicate is defined (protectPred != null)
					// 2. the keeper is not modifiable (mod == null)
					toKeep.add(Fun.pred(protectPred, n, objVar));

				if (mod == null && n.getType().isArray()
						&& n.getType().getComponentType().isArray()
						&& 0 < k.getValue().length && k.getValue()[0] != null
						&& k.getValue()[0].isProtection()) {
					// protect arrays nested into keeper arrays TODO multi-layer nesting
					// TODO encode in "protect"-like predicate so we can use forall quantification?
					Integer objInc = safeGet(arrays, objType);
					if (objInc != null) {
						Local indexJ = new Local("j'", intType);
						toKeep.add(Infix.and(Prefix.not(Infix.equals(n, Literal.NULL)), Quantifier.exists(
								indexJ,
								Infix.equals(
										new Select(n, indexJ, objType, objInc),
										objVar))));
					}
				}
			}

			ITypeBinding heapType = h.getKey();
			result.add(Quantifier.forall(
					Arrays.asList(objVar, indexVar),
					Infix.toInfix(Operator.OR,
							Prefix.not(Infix.toInfix(Operator.OR, toKeep)),
							Infix.equals(
									new Select(objVar, indexVar, heapType, oldIncarnation),
									new Select(objVar, indexVar, heapType, newIncarnation)))));
			// TODO protect arrays inside other arrays according to elems attribute
		}
		// TODO havoc static fields
		return result;
	}

	/**
	 * Override this method if there's a protection predicate for the given heap.
	 * This will be used as an additional condition for when arrays do not change.
	 * @param heap {@link #getHeapType(ITypeBinding) Heap type}
	 * @return predicate name or {@code null} if no such predicate exists
	 */
	protected String getProtectionPredicate(ITypeBinding heap) {
		return null;
	}

	/**
	 * Returns formulae to identify the given "keepers" as well as
	 * objects the keepers protect with field permissions,
	 * except if those objects are also reachable from the given
	 * modifiable objects.
	 * Protected objects are only included if {@link #getProtectionPredicate(ITypeBinding)}
	 * returns non-{@code null} for {@link #objType}bears.
	 * @param objVar variable to equate the objects we want with
	 * (this is usually a quantification variable).
	 * @param keep objects to keep with their array permissions, if applicable
	 * (these are usually objects for which we have permissions in the local scope)
	 * @param haveModifiablePermission modifiable objects, i.e.,
	 * parameters declared to have a modifiable permission such as Excl
	 * @return formulae to identify objects to keep
	 */
	protected final Set<Formula> keepPredicate(Local objVar,
			Map<Name, PermKind[]> keep,
			Set<Name> haveModifiablePermission) {
		Set<Formula> toKeep = new LinkedHashSet<Formula>();
		String protectPred = getProtectionPredicate(objType);
		Set<Formula> toProtect;
		if (protectPred == null)
			toProtect = null;
		else if (haveModifiablePermission.isEmpty())
			// optimization: if there are no modifiable fields we can
			// add protection predicates directly to toKeep formulae
			toProtect = toKeep;
		else
			toProtect = new LinkedHashSet<Formula>();

		for (Map.Entry<Name, PermKind[]> k : keep.entrySet()) {
			Name n = k.getKey();
			toKeep.add(Infix.equals(n, objVar));
			if (protectPred != null && ! haveModifiablePermission.contains(n))
				// optimization: don't even try protecting n's fields
				// if n itself is literally in modifiableFields
				// may not always work as n may not be the only way to get
				// to the referenced object, hence the extra formula below
				// that explicitly requires protected objects to not be
				// in the modifiable set
				toProtect.add(Fun.pred(protectPred, n, objVar));

			// see havocArrays: protect objects reachable through
			// keeper arrays with permissions for all dimensions
			PermKind[] dims = k.getValue();
			array_protects_objects:
			if (! haveModifiablePermission.contains(n) && n.getType().isArray()
					&& 0 < dims.length) {
				Integer objInc = safeGet(arrays, objType);
				if (objInc == null)
					break array_protects_objects;

				// determine whether this is a (nested) array of objects
				// with permissions for all array dimensions
				ITypeBinding component = n.getType().getComponentType();
				for (int i = 0; i < dims.length; ++i) {
					if (dims[i] == null || !dims[i].isProtection())
						break array_protects_objects;
					if (component.isArray())
						component = component.getComponentType();
					else if (i != dims.length - 1)
						// array depth and protecting permissions depth don't match (specification error)
						break array_protects_objects;
				}
				if (component.isArray() || component.isPrimitive())
					// permissions don't cover all dimensions or array of primitives
					break array_protects_objects;

				// put together nested "exists" formulae
				// TODO encode in "protect"-like predicate so we can use forall quantification?
				Local[] indices = new Local[dims.length];
				Name[] objects = new Name[dims.length];
				objects[0] = n;
				Formula f = null;
				for (int i = dims.length-1; 0 <= i; --i) {
					indices[i] = new Local("j" + i + "'", intType);
					if (i != 0)
						objects[i] = new Local("a" + i + "'", objType);
					if (i == dims.length - 1)
						f = Infix.and(Prefix.not(Infix.equals(objects[i], Literal.NULL)),
								Quantifier.exists(
										indices[i],
										Infix.equals(
												new Select(objects[i], indices[i], objType, objInc),
												objVar)));
					else
						f = Infix.and(Prefix.not(Infix.equals(objects[i], Literal.NULL)),
								Quantifier.exists(
										Arrays.asList(indices[i], (Local) objects[i + 1]),
										Infix.and(
											Infix.equals(
												new Select(objects[i], indices[i], objType, objInc),
												objects[i + 1]),
											f)));
				}
				toKeep.add(f);
			}
		}
		// protect fields transitively except where modifiable
		if (toProtect != null && ! toProtect.isEmpty() && ! haveModifiablePermission.isEmpty()) {
			// toProtect != null implies protectPred != null
			Set<Formula> exclude = new LinkedHashSet<Formula>();
			for (Name m : haveModifiablePermission)
				// exclude any object reachable through objects with modifiable fields
				exclude.add(Fun.pred(protectPred, m, objVar));
			toKeep.add(Infix.toInfix(Operator.AND,
					Prefix.not(Infix.toInfix(Operator.OR, exclude)),
					Infix.toInfix(Operator.OR, toProtect)));
		}
		return toKeep;
	}

	protected final Collection<Formula> havocArrayCell(ArrayAccess a, boolean aroundLoop) {
		ITypeBinding heapType = getHeapType(a.resolveTypeBinding());
		Integer incarnation = safeGet(arrays, heapType);
		if (incarnation == null)
			return Collections.emptySet();

		Formula array = ExpressionEncoder.encode(a.getArray(), this);
		Formula index = ExpressionEncoder.encode(a.getIndex(), this);

		// havoc array heap...
		int newInc = incarnation + 1;
		arrays.put(heapType, newInc);

		Local arrayVar = new Local("a'", objType);
		Local indexVar = new Local("i'", intType);

		// ... and equate every array cell except modified cells with old heap
		Formula mayChange = Infix.equals(array, arrayVar);
		if (! aroundLoop) {
			// be precise: only the indexed cell is changing
			mayChange = Infix.toInfix(Operator.AND,
				mayChange,
				Infix.equals(index, indexVar));
		} // else assume any cell could have changed
		Formula result = Quantifier.forall(
				Arrays.asList(arrayVar, indexVar),
				Infix.toInfix(Operator.OR,
						mayChange,
						Infix.equals(
								new Select(arrayVar, indexVar, a.resolveTypeBinding(), incarnation),
								new Select(arrayVar, indexVar, a.resolveTypeBinding(), newInc))));

		return Collections.singleton(result);
	}


	/**
	 * Maps primitives to normalized versions of themselves and
	 * object and array primitives to {@link #objType}.
	 * Normalization involves using only types from the current AST,
	 * which is necessary to use types as map keys because otherwise
	 * {@link ITypeBinding#equals(Object)} doesn't work quite right.
	 * @param t
	 * @return heap type for the given type, always from the current AST
	 */
	protected final ITypeBinding getHeapType(ITypeBinding t) {
		return types.getHeapType(t);
	}

	/**
	 * Use this method to call {@link Map#get(Object)} on
	 * {@link ITypeBinding}-indexed maps to make sure you use keys normalized
	 * with {@link #getHeapType(ITypeBinding)}.
	 * If {@code get} returns {@code null} this method checks if {@code map}
	 * does contain a value for the normalized version of {@code key} and
	 * throws if it does.
	 * @param <V>
	 * @param map
	 * @param key
	 * @return the result of {@link Map#get(Object)}
	 * @throws IllegalArgumentException if the given key seemingly was not normalized
	 */
	protected final <V> V safeGet(Map<ITypeBinding, ? extends V> map,
			ITypeBinding key) {
		V result = map.get(key);
		if (result == null) {
			ITypeBinding normalized = getHeapType(key);
			if (map.get(normalized) != null)
				throw new IllegalArgumentException("Type key was not normalized: " + key);
		}
		return result;
	}

	public Local getReceiver(ITypeBinding type) {
		return new Local(Contract.THIS_VAR_NAME, type);
	}

	/**
	 * Returns the given variable ref's local
	 * @param var must be a local variable access, not a field or method name
	 * @return
	 */
	private Local getLocal(SimpleName var) {
		IVariableBinding binding = (IVariableBinding) var.resolveBinding();
		binding = binding.getVariableDeclaration();
		return getLocal(binding);
	}

	/**
	 * Returns the given variable ref's local
	 * @param var must be a local variable access, not a field or method name
	 * @return
	 */
	public Local getLocal(IVariableBinding var) {
		if (var.isField() || var.isEnumConstant())
			throw new IllegalArgumentException("Not a local: " + var);
		Integer result = locals.get(var);
		if (result == null) {
			result = 0;
			locals.put(var, result);
		}
		return new Local(var, result);
	}

	/**
	 * Resolves the given expression to a field or local
	 * @param e
	 * @return {@code null} if expression does not resolve to field or local,
	 * in particular in case this is a method's <i>name</i> or an enum constant.
	 */
	public Name getName(Expression e) {
		if (e instanceof SimpleName) {
			SimpleName var = (SimpleName) e;
			if (! (var.resolveBinding() instanceof IVariableBinding))
				return null; // method or other name
			IVariableBinding binding = (IVariableBinding) var.resolveBinding();
			if (binding.isField()) {
				if (Modifier.isStatic(binding.getModifiers()))
					throw new UnsupportedOperationException("cannot encode " + e);
				return getField(null, binding);
			} else if (binding.isEnumConstant()) {
				return null;
			} else { // local
				return getLocal(var);
			}
		}
		if (e instanceof QualifiedName) {
			QualifiedName f = (QualifiedName) e;
			Name access = getName(f.getQualifier());
			return getField(access, (IVariableBinding) f.resolveBinding());
		}
		if (e instanceof FieldAccess) {
			FieldAccess f = (FieldAccess) e;
			Name access = getName(f.getExpression());
			return getField(access, f.resolveFieldBinding());
		}
		if (e instanceof ParenthesizedExpression)
			return getName(((ParenthesizedExpression) e).getExpression());
		if (e instanceof Assignment)
			return getName(((Assignment) e).getRightHandSide());
		return getLocal(e);
	}

	@Override
	public Select getSelect(Formula array, Formula index, ITypeBinding elementType) {
		ITypeBinding heapType = getHeapType(elementType);
		Integer incarnation = safeGet(arrays, heapType);
		if (incarnation == null) {
			incarnation = 0;
			arrays.put(heapType, incarnation);
		}
		return new Select(array, index, elementType, incarnation);
	}

	/**
	 * merge l2 into l1 and l1 into l2: both lookups should be equal afterwards
	 * @param <L> concrete lookup type
	 * @param l1
	 * @param k1
	 * @param l2
	 * @param k2
	 */
	public static <L extends AbstractHavocLookup<L>>
	void mergeLookups(L l1, Set<Formula> k1, L l2, Set<Formula> k2) {
		// avoid symmetric cases we simply merge l2 into l1 and l1 into l2
		// both lookups should be equal afterwards
		l1.mergeLookups(k1, l2);
		l2.mergeLookups(k2, l1);
	}

	/**
	 * Override this method to perform additional merging...
	 * @param knowledge knowledge based on receiver's lookup info
	 * @param other other lookup
	 */
	protected void mergeLookups(Set<Formula> knowledge, T other) {
		if (this.temps != other.temps)
			throw new IllegalArgumentException();
		for (Entry<IVariableBinding, Integer> local1 : this.locals.entrySet()) {
			IVariableBinding var = local1.getKey();
			Integer i1 = local1.getValue();
			Integer i2 = other.locals.get(var);
			if (i2 != null) {
				if (i1 < i2) {
					equate(knowledge, this.getLocal(var), other.getLocal(var));
					local1.setValue(i2);
				} // else symmetric call will kick in
			} else {
				other.locals.put(var, i1);
			}
		}

		for (Entry<ITypeBinding, Integer> array1 : this.arrays.entrySet()) {
			ITypeBinding cellType = array1.getKey();
			Integer i1 = array1.getValue();
			Integer i2 = safeGet(other.arrays, cellType);
			if (i2 != null) {
				if (i1 < i2) {
					Local arrayVar = new Local("a'", objType);
					Local indexVar = new Local("i'", intType);
					knowledge.add(Quantifier.forall(
							Arrays.asList(arrayVar, indexVar),
							Infix.equals(
									new Select(arrayVar, indexVar, cellType, i1),
									new Select(arrayVar, indexVar, cellType, i2))));
					array1.setValue(i2);
				} // else symmetric call will kick in
			} else {
				other.arrays.put(cellType, i1);
			}
		}
	}

	/**
	 * Equates the two given names by extending the given knowledge
	 * @param knowledge
	 * @param l1
	 * @param l2
	 */
	protected static void equate(Set<Formula> knowledge, Name l1, Name l2) {
		knowledge.add(Infix.equals(l1, l2));
	}

	/**
	 * This class encapsulates type normalization so type bindings are usable
	 * as map keys.
	 * Type bindings from different ASTs are incomparable, leading to problems
	 * when looking up values from maps using such bindings.
	 * This class currently turns type bindings from any AST into
	 * type bindings from a particular AST.
	 * @author kevin
	 * @since Jan 9, 2011
	 */
	private static class TypeNormalizer {

		private final AST ast;
		/** {@link Object}'s type binding in {@link #ast} */
		private final ITypeBinding objType;
		/** primitive type bindings in {@link #ast} */
		private final Map<String, ITypeBinding> primitives =
			new HashMap<String, ITypeBinding>();

		public TypeNormalizer(AST ast) {
			super();
			this.ast = ast;
			this.objType = ast.resolveWellKnownType(Object.class.getName());
		}

		public ITypeBinding getObjectType() { return objType; }

		public ITypeBinding getHeapType(ITypeBinding type) {
			if (! type.isPrimitive())
				return objType;

			// use primitive type binding from given AST no matter what
			String name = type.getName();
			ITypeBinding result = primitives.get(name);
			if (result == null) {
				result = ast.resolveWellKnownType(name);
				primitives.put(name, result);
			}
			return result;
		}
	}
}
